$\forall$${\it es}$:ES, $C$:Type, ${\it in}$:($C$$\rightarrow$IdLnk), $m$, ${\it req}$:Id, $j$, $i$:$C$, $e$:E.
\\[0ex]((kindtype(destination(${\it in}$($j$));rcv(${\it in}$($j$),$m$)) $\subseteq$r (:($C$ List) $\times$ Top))
\\[0ex]\& (kindtype(destination(${\it in}$($j$));rcv(${\it in}$($j$),${\it req}$)) $\subseteq$r (:($C$ List) $\times$ Top)))
\\[0ex]$\Rightarrow$ (fifo+send(${\it es}$;$C$;${\it in}$;$m$;${\it req}$;$j$;$i$;$e$) $\in$ $\mathbb{P}$)